(set-logic QF_BV)
(declare-fun x () (_ BitVec 4))
(declare-fun y () (_ BitVec 2))
(declare-fun z () (_ BitVec 4))
(assert (= x ((_ sign_extend 2) y)))
(assert (= false (bvsle (_ bv0 4) z)))
(assert (= false (bvule x z)))
(check-sat)
(exit)
